$\forall$$A$:Type, $l$:($A$ List). tl($l$) $\in$ ($A$ List)